Enable Kepler-formal LEC for multiple designs#3985
Open
openroad-ci wants to merge 18 commits intoThe-OpenROAD-Project:masterfrom
Open
Enable Kepler-formal LEC for multiple designs#3985openroad-ci wants to merge 18 commits intoThe-OpenROAD-Project:masterfrom
openroad-ci wants to merge 18 commits intoThe-OpenROAD-Project:masterfrom
Conversation
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
- Previously, KF for those designs were disabled due to KF & OR issues Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Add LEC_AUX_VERILOG_FILES support to lec_check.tcl so that auxiliary Verilog files (e.g., blackbox module stubs) are concatenated into LEC netlists before Kepler Formal runs. For sky130hd/chameleon, provide clean blackbox stubs for DFFRAM_4K, DMC_32x16HC, ibex_wrapper, and apb_sys_0 so KF can resolve these macro modules during CTS LEC. Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Update OpenROAD to 9b0caf1a52 which includes the unified makeNewNetName fix, resolving wire collision for hierarchical designs (e.g., microwatt CTS LEC "wire collision for net net"). Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
openroad-ci
force-pushed
the
secure-enable-kf-lec-check
branch
from
69ef0a2 to
f6508cc
Compare
KF crashes with assertion failure in SNLLogicCloud.cpp:349: "Iso have no drivers and more than one reader, not supported" Both base and verific variants affected. Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Widen globalroute and finish setup TNS thresholds from -697 to -750 to accommodate timing change from OR 9b0caf1a52 (makeNewNetName). Actual: -727.5 (4.4% regression). Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Widen area and TNS thresholds for gcd, ibex, ethmac, jpeg to accommodate changes from OR 9b0caf1a52 (makeNewNetName). Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
cva6/verific: widen stdcell count (173997→183000), CTS WS (-0.14→-0.15) hercules_idecode/verific: widen CTS/GRT/finish TNS thresholds for timing regression from OR 9b0caf1a52. Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Empty commit to retrigger sync and Jenkins PR-merge build. Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
…ate/OpenROAD-flow-scripts into secure-enable-kf-lec-check Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
The bumped kepler-formal still has bugs for these designs: - nangate45/mempool_group: assertion crash in SNLLogicCloud.cpp:349 "Iso have no drivers and more than one reader, not supported" - rapidus2hp/cva6: netlist loading failure bus net "icache_areq_o" cannot be found in ALU module Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
designs/rapidus2hp/cva6/rules-base.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | globalroute__timing__setup__tns | -452.0 | -463.0 | Failing | | finish__timing__setup__tns | -452.0 | -463.0 | Failing | designs/rapidus2hp/cva6/rules-verific.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | placeopt__design__instance__count__stdcell | 201058 | 200149 | Tighten | | cts__timing__setup__ws | -0.136 | -0.167 | Failing | | finish__timing__setup__tns | -550.0 | -738.0 | Failing | Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
designs/nangate45/swerv_wrapper/rules-base.json updates: | Metric | Old | New | Type | | ------ | --- | --- | ---- | | cts__timing__setup__ws | -0.197 | -0.466 | Failing | | cts__timing__setup__tns | -84.6 | -290.0 | Failing | | globalroute__timing__setup__tns | -86.3 | -211.0 | Failing | | detailedroute__route__wirelength | 5546498 | 4367567 | Tighten | | finish__timing__setup__tns | -88.2 | -198.0 | Failing | Signed-off-by: Jaehyun Kim <jhkim@precisioninno.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #3953